T:Type, f:((T List)), t, t':.
t<t'  concat(map(f;upto(t))) @ (f(t))  concat(map(f;upto(t'))) 

latex

Definitions	S  T, i  j < k, S  T, Top, {i..j}, Unit, P  Q, P & Q, i=j, , b, b, as @ bs, concat(ll), map(f;as), upto(n), AB, A, False, P  Q, l1  l2, Prop, x:A. B(x), , t  T
Lemmas	nat wf, assert wf, not wf, bnot wf, bool wf, eq int wf, assert of eq int, not functionality wrt iff, assert of bnot, iff transitivity, eqff to assert, eqtt to assert, upto wf, int seg wf, map append sq, le wf, top wf, map wf, concat append, append nil sq, concat-cons, concat iseg, iseg map, upto iseg